es.locl("b") sends ["tg",x.x{}("done")] on link lnk1{loc1 to loc2} once 

latex

Definitions	A & B, P & Q, Id, t  T, Normal(T), IdLnk, lnk$n{$a to $b}, "$x", P  Q, x:A. B(x)
Lemmas	bool-inhabited, bool wf, send-once-realizable